Inference at * 1 
Iof proof for Lemma dep ax choice:



1. A : Type
2. B : AType
3. Q : x:AB(x)Type
4. x:A. y:B(x). Q(x,y)
  f:x:AB(x). (x:A. Q(x,f(x))) 

latex

 by ((Unfolds ``all exists`` 4) 
CollapseTHEN (RenameVar `g' 4)) 

latex

C1: 

C1: 4. x:Ay:B(x)  Q(x,y)
C1:   f:x:AB(x). (x:A. Q(x,f(x)))
C.

Definitions

x:A. B(x), x:A. B(x)